A:es_realizer{i:l}. R-Feasible{i:l}(A)  R-compat{i:l}(A; A) 

latex

Definitions

ge(i; j), False, A, A  B, x. t(x), ff, tt, True, P  Q, if b then t else f fi , Y, prop{i:l}, t  T, R-compat{i:l}(A; B), P  Q, x:A. B(x), , x(s), guard(T), P  Q, P  Q, Unit, , , R-Feasible{i:l}(R), , subtype(S; T)

Lemmas

R-base-domain wf, eq bd wf, not functionality wrt iff, assert-eq-id, R-loc wf, eq id wf, ge wf, nat properties, R-interface-compat-self, R-discrete compat self, R-frame-compat-self, Rda wf, Kind-deq wf, Knd wf, Rds wf, id-deq wf, Id wf, fpf-compatible-self, Rnone? wf, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, R-compat-symmetry, Rplus-right wf, Rplus-left wf, R-compat-Rplus2, R-size-decreases, Rplus-implies, eqtt to assert, bool wf, Rplus? wf, le wf, es realizer wf, R-Feasible wf, nat plus wf, nat plus inc, R-size wf, nat wf